可满足性问题（SAT）是一种NP完全问题，被广泛运用于人工智能和机器学习等研究。恰当可满足性问题（XSAT）是SAT中一类重要的子问题。目前的大部分关于XSAT的研究主要为理论层面，对高效的求解算法特别是具有高效验证性的随机局部搜索算法研究很少。针对以上问题，分析了基础编码和等价编码两种转化方式的公式的部分性质，提出一种直接求解XSAT的随机局部搜索算法WalkXSAT。首先使用随机局部搜索框架进行基础搜索与条件判定；其次加入变元所属文字的恰当不可满足计分值，优先处理不易恰当满足的变元；然后使用防重复选择翻转变元的启发式策略减小搜索空间；最后，采用多种来源以及多种格式的实例进行对比实验。在直接求解XSAT时，相较于ProbSAT，WalkXSAT的变元翻转次数与求解时间显著减少；在求解基础编码转化后的实例中，当实例变元规模大于100时，ProbSAT已失效，而WalkXSAT依然能够在短时间内求解。实验结果表明，所提WalkXSAT精确性高、稳定性强、收敛快。
